1  /-
  2  Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel
  5  -/
  6  
  7  import linear_algebra.basic
src         └──────────────────┘
  8  
  9  /-!
 10  # Multilinear maps
 11  
 12  We define multilinear maps as maps from `Π(i : ι), M₁ i` to `M₂` which are linear in each
 13  coordinate. Here, `M₁ i` and `M₂` are modules over a ring `R`, and `ι` is an arbitrary type
 14  (although some statements will require it to be a fintype). This space, denoted by
 15  `multilinear_map R M₁ M₂`, inherits a module structure by pointwise addition and multiplication.
 16  
 17  ## Main definitions
 18  
 19  * `multilinear_map R M₁ M₂` is the space of multilinear maps from `Π(i : ι), M₁ i` to `M₂`.
 20  * `f.map_smul` is the multiplicativity of the multilinear map `f` along each coordinate.
 21  * `f.map_add` is the additivity of the multilinear map `f` along each coordinate.
 22  * `f.map_smul_univ` expresses the multiplicativity of `f` over all coordinates at the same time,
 23    writing `f (λi, c i • m i)` as `univ.prod c • f m`.
 24  * `f.map_add_univ` expresses the additivity of `f` over all coordinates at the same time, writing
 25    `f (m + m')` as the sum over all subsets `s` of `ι` of `f (s.piecewise m m')`.
 26  
 27  We also register isomorphisms corresponding to currying or uncurrying variables, transforming a
 28  multilinear function `f` on `n+1` variables into a linear function taking values in multilinear
 29  functions in `n` variables, and into a multilinear function in `n` variables taking values in linear
 30  functions. These operations are called `f.curry_left` and `f.curry_right` respectively
 31  (with inverses `f.uncurry_left` and `f.uncurry_right`). These operations induce linear equivalences
 32  between spaces of multilinear functions in `n+1` variables and spaces of linear functions into
 33  multilinear functions in `n` variables (resp. multilinear functions in `n` variables taking values
 34  in linear functions), called respectively `multilinear_curry_left_equiv` and
 35  `multilinear_curry_right_equiv`.
 36  
 37  ## Implementation notes
 38  
 39  Expressing that a map is linear along the `i`-th coordinate when all other coordinates are fixed
 40  can be done in two (equivalent) different ways:
 41  * fixing a vector `m : Π(j : ι - i), M₁ j.val`, and then choosing separately the `i`-th coordinate
 42  * fixing a vector `m : Πj, M₁ j`, and then modifying its `i`-th coordinate
 43  The second way is more artificial as the value of `m` at `i` is not relevant, but it has the
 44  advantage of avoiding subtype inclusion issues. This is the definition we use, based on
 45  `function.update` that allows to change the value of `m` at `i`.
 46  -/
 47  
 48  open function fin set
 49  
 50  universes u v v' w u'
 51  variables {R : Type u} {ι : Type u'} {n : ℕ} {M : fin n.succ → Type v'} {M₁ : ι → Type v} {M₂ : Type w}
id                                                    └─┘  └───┘
src                                                   └─┘  └───┘
typ                                                   └─┘  └───┘
 52  [decidable_eq ι]
id    └──────────┘
src   └──────────┘
typ   └──────────┘
 53  
 54  /-- Multilinear maps over the ring `R`, from `Πi, M₁ i` to `M₂` where `M₁ i` and `M₂` are modules
 55  over `R`. -/
 56  structure multilinear_map (R : Type u) {ι : Type u'} (M₁ : ι → Type v) (M₂ : Type w)
id                                  └──┘         └──┘                           └──┘
typ                                 └──┘         └──┘                           └──┘
 57    [decidable_eq ι] [ring R] [∀i, add_comm_group (M₁ i)] [add_comm_group M₂] [∀i, module R (M₁ i)]
id      └──────────┘    └──┘       └────────────┘  └┘     └────────────┘ └┘      └────┘   └┘ 
src     └──────────┘     └──┘         └────────────┘          └────────────┘          └────┘
typ     └──────────┘    └──┘       └────────────┘  └┘     └────────────┘ └┘      └────┘   └┘ 
doc                                                                                   └────┘
 58    [module R M₂] :=
id      └────┘  └┘
src     └────┘
typ     └────┘  └┘
doc     └────┘
 59  (to_fun : (Πi, M₁ i) → M₂)
id                 └┘    └┘
typ                └┘    └┘
 60  (add : ∀(m : Πi, M₁ i) (i : ι) (x y : M₁ i),
id                  └┘                 └┘ 
typ                 └┘                 └┘ 
 61    to_fun (update m i (x + y)) = to_fun (update m i x) + to_fun (update m i y))
id     └────┘  └────┘          └────┘  └────┘      └────┘  └────┘   
src            └────┘                      └────┘                 └────┘
typ    └────┘  └────┘          └────┘  └────┘      └────┘  └────┘   
doc            └────┘                        └────┘                  └────┘
 62  (smul : ∀(m : Πi, M₁ i) (i : ι) (c : R) (x : M₁ i),
id                   └┘                      └┘ 
typ                  └┘                      └┘ 
 63    to_fun (update m i (c • x)) = c • to_fun (update m i x))
id     └────┘  └────┘            └────┘  └────┘   
src            └────┘                         └────┘
typ    └────┘  └────┘            └────┘  └────┘   
doc            └────┘                            └────┘
 64  
 65  namespace multilinear_map
 66  
 67  section ring
 68  
 69  variables [ring R] [∀i, add_comm_group (M i)] [∀i, add_comm_group (M₁ i)] [add_comm_group M₂]
id              └──┘        └────────────┘           └────────────┘         └────────────┘
src             └──┘         └────────────┘             └────────────┘          └────────────┘
typ             └──┘        └────────────┘           └────────────┘         └────────────┘
 70  [∀i, module R (M i)] [∀i, module R (M₁ i)] [module R M₂]
id       └────┘             └────┘           └────┘
src       └────┘               └────┘            └────┘
typ      └────┘             └────┘           └────┘
doc       └────┘               └────┘            └────┘
 71  (f f' : multilinear_map R M₁ M₂)
id           └─────────────┘
src          └─────────────┘
typ          └─────────────┘
doc          └─────────────┘
 72  
 73  instance : has_coe_to_fun (multilinear_map R M₁ M₂) := ⟨_, to_fun⟩
id              └────────────┘  └─────────────┘  └┘ └┘         └────┘
src             └────────────┘  └─────────────┘                 └────┘
typ             └────────────┘  └─────────────┘  └┘ └┘         └────┘
doc                             └─────────────┘
 74  
 75  @[ext] theorem ext {f f' : multilinear_map R M₁ M₂} (H : ∀ x, f x = f' x) : f = f' :=
id                              └─────────────┘  └┘ └┘              └┘       └┘
src                             └─────────────┘                                   
typ                             └─────────────┘  └┘ └┘              └┘       └┘
doc    └─┘                      └─────────────┘
 76  by cases f; cases f'; congr'; exact funext H
id                    └┘                └────┘ 
src     └────┘   └────┘    └────┘  └────┘└────┘ 
typ     └────┘  └────┘└┘  └────┘  └────┘└────┘
doc     └────┘   └────┘    └────┘  └────┘       
txt     └────┘   └────┘    └────┘  └────┘       
par     └────┘   └────┘    └────┘  └────┘       
pid                                          
st     └──────────────────────────────────────────
 77  
src  
typ  
doc  
txt  
par  
pid  
st   
 78  @[simp] lemma map_add (m : Πi, M₁ i) (i : ι) (x y : M₁ i) :
id                                 └┘                 └┘ 
typ                                └┘                 └┘ 
doc    └──┘
 79    f (update m i (x + y)) = f (update m i x) + f (update m i y) :=
id       └────┘            └────┘        └────┘   
src       └────┘                 └────┘            └────┘
typ      └────┘            └────┘        └────┘   
doc       └────┘                   └────┘             └────┘
 80  f.add m i x y
id   └──┘    
src   └──┘
typ  └──┘    
 81  
 82  @[simp] lemma map_smul (m : Πi, M₁ i) (i : ι) (c : R) (x : M₁ i) :
id                                  └┘                      └┘ 
typ                                 └┘                      └┘ 
doc    └──┘
 83    f (update m i (c • x)) = c • f (update m i x) :=
id       └────┘              └────┘   
src       └────┘                    └────┘
typ      └────┘              └────┘   
doc       └────┘                       └────┘
 84  f.smul m i c x
id   └───┘    
src   └───┘
typ  └───┘    
 85  
 86  @[simp] lemma map_sub (m : Πi, M₁ i) (i : ι) (x y : M₁ i) :
id                                 └┘                 └┘ 
typ                                └┘                 └┘ 
doc    └──┘
 87    f (update m i (x - y)) = f (update m i x) - f (update m i y) :=
id       └────┘            └────┘        └────┘   
src       └────┘                 └────┘            └────┘
typ      └────┘            └────┘        └────┘   
doc       └────┘                   └────┘             └────┘
 88  by { simp only [map_add, add_left_inj, sub_eq_add_neg, (neg_one_smul R y).symm, map_smul], simp }
id                   └─────┘  └──────────┘  └────────────┘   └──────────┘          └──────┘
src       └─────────┘└─────┘└┘└──────────┘└┘└────────────┘└┘ └──────────┘  └──────┘└──────┘  └───┘
typ       └─────────┘└─────┘└┘└──────────┘└┘└────────────┘└┘ └──────────┘└──────┘└──────┘  └───┘
doc       └─────────┘       └┘            └┘              └┘               └──────┘          └───┘
txt       └─────────┘       └┘            └┘              └┘               └──────┘          └───┘
par       └─────────┘       └┘            └┘              └┘               └──────┘          └───┘
pid           └──┘└┘       └┘            └┘              └┘               └──────┘              
st     └─────────────────────────────────────────────────────────────────────────────────────┘└─────┘└┘
 89  
 90  lemma map_coord_zero {m : Πi, M₁ i} (i : ι) (h : m i = 0) : f m = 0 :=
id                                └┘                         
src                                                                 
typ                               └┘                         
 91  begin
st   └─────
 92    have : (0 : R) • (0 : M₁ i) = 0, by simp,
id                         └┘   
src    └─────┘ └──┘ └┘ └──┘   └┘└┘     └──┘
typ    └─────┘ └──┘└┘ └──┘└┘└┘└┘     └──┘
doc    └─────┘ └──┘ └┘  └──┘   └┘ └┘     └──┘
txt    └─────┘ └──┘ └┘  └──┘   └┘ └┘     └──┘
par    └─────┘ └──┘ └┘  └──┘   └┘ └┘     └──┘
pid    └───┘└┘ └──┘ └┘  └──┘   └┘ 
st   ────────────────────────────────┘         └─
 93    rw [← update_eq_self i m, h, ← this, f.map_smul, zero_smul]
id           └────────────┘        └──┘              └───────┘
src    └────┘└────────────┘  └┘ └──┘    └┘          └┘└───────┘└┘
typ    └────┘└────────────┘└┘└──┘└──┘└┘└────────┘└┘└───────┘└┘
doc    └────┘                └┘ └──┘    └┘          └┘         └┘
txt    └────┘                └┘ └──┘    └┘          └┘         └┘
par    └────┘                └┘ └──┘    └┘          └┘         └┘
pid      └──┘                └┘ └──┘    └┘          └┘         
st   ─────────────────────────┘└─┘└──────┘└──────────┘└─────────┘
 94  end
st   └─┘
 95  
 96  @[simp] lemma map_zero [nonempty ι] : f 0 = 0 :=
id                           └──────┘        
src                          └──────┘          
typ                          └──────┘        
doc    └──┘
 97  begin
st   └─────
 98    obtain ⟨i, _⟩ : ∃i:ι, i ∈ set.univ := set.exists_mem_of_nonempty ι,
id                            └──────┘    └────────────────────────┘ 
src    └──────────────┘└┘  └──────┘└──┘└────────────────────────┘
typ    └──────────────┘└┘  └──────┘└──┘└────────────────────────┘
doc    └──────────────┘ └┘            └──┘                          
txt    └──────────────┘ └┘            └──┘                          
par    └──────────────┘ └┘            └──┘                          
pid          └────────┘ └┘            └──┘                          
st   ───────────────────────────────────────────────────────────────────┘└─
 99    exact map_coord_zero f i rfl
id           └────────────┘   └─┘
src    └────┘└────────────┘  └─┘
typ    └────┘└────────────┘└─┘
doc    └────┘                   
txt    └────┘                   
par    └────┘                   
pid                            
st   ──────────────────────────────┘
100  end
st   └─┘
101  
102  instance : has_add (multilinear_map R M₁ M₂) :=
id              └─────┘  └─────────────┘  └┘ └┘
src             └─────┘  └─────────────┘
typ             └─────┘  └─────────────┘  └┘ └┘
doc                      └─────────────┘
103  ⟨λf f', ⟨λx, f x + f' x, λm i x y, by simp, λm i c x, by simp [smul_add]⟩⟩
id      └┘         └┘                                 └──────┘
src                                       └──┘               └────┘└──────┘
typ     └┘         └┘            └──┘           └────┘└──────┘
doc                                        └──┘               └────┘        
txt                                        └──┘               └────┘        
par                                        └──┘               └────┘        
pid                                                                       
st                                        └───┘              └──────────────┘
104  
105  @[simp] lemma add_apply (m : Πi, M₁ i) : (f + f') m = f m + f' m := rfl
id                                   └┘        └┘       └┘     └─┘
src                                                                   └─┘
typ                                  └┘        └┘       └┘     └─┘
doc    └──┘
106  
107  instance : has_neg (multilinear_map R M₁ M₂) :=
id              └─────┘  └─────────────┘  └┘ └┘
src             └─────┘  └─────────────┘
typ             └─────┘  └─────────────┘  └┘ └┘
doc                      └─────────────┘
108  ⟨λ f, ⟨λ m, - f m, λm i x y, by simp, λm i c x, by simp⟩⟩
id                                    
src                                 └──┘               └──┘
typ                         └──┘           └──┘
doc                                  └──┘               └──┘
txt                                  └──┘               └──┘
par                                  └──┘               └──┘
st                                  └───┘              └───┘
109  
110  @[simp] lemma neg_apply (m : Πi, M₁ i) : (-f) m = - (f m) := rfl
id                                   └┘                  └─┘
src                                                            └─┘
typ                                  └┘                  └─┘
doc    └──┘
111  
112  instance : has_zero (multilinear_map R M₁ M₂) :=
id              └──────┘  └─────────────┘  └┘ └┘
src             └──────┘  └─────────────┘
typ             └──────┘  └─────────────┘  └┘ └┘
doc                       └─────────────┘
113  ⟨⟨λ _, 0, λm i x y, by simp, λm i c x, by simp⟩⟩
id                               
src                         └──┘               └──┘
typ                    └──┘           └──┘
doc                         └──┘               └──┘
txt                         └──┘               └──┘
par                         └──┘               └──┘
st                         └───┘              └───┘
114  
115  instance : inhabited (multilinear_map R M₁ M₂) := ⟨0⟩
id              └───────┘  └─────────────┘  └┘ └┘
src             └───────┘  └─────────────┘
typ             └───────┘  └─────────────┘  └┘ └┘
doc                        └─────────────┘
116  
117  @[simp] lemma zero_apply (m : Πi, M₁ i) : (0 : multilinear_map R M₁ M₂) m = 0 := rfl
id                                    └┘          └─────────────┘  └┘ └┘         └─┘
src                                                 └─────────────┘                  └─┘
typ                                   └┘          └─────────────┘  └┘ └┘         └─┘
doc    └──┘                                         └─────────────┘
118  
119  instance : add_comm_group (multilinear_map R M₁ M₂) :=
id              └────────────┘  └─────────────┘  └┘ └┘
src             └────────────┘  └─────────────┘
typ             └────────────┘  └─────────────┘  └┘ └┘
doc                             └─────────────┘
120  by refine {zero := 0, add := (+), neg := has_neg.neg, ..};
id                                           └─────────┘
src     └─────┘ └────────────────┘└─────────┘└─────────┘└───┘
typ     └─────┘ └────────────────┘└─────────┘└─────────┘└───┘
doc     └─────┘ └────────────────┘ └─────────┘           └───┘
txt     └─────┘ └────────────────┘ └─────────┘           └───┘
par     └─────┘ └────────────────┘ └─────────┘           └───┘
pid            └────────────────┘ └─────────┘           └───┘
st     └────────────────────────────────────────────────────────
121     intros; ext; simp
src     └────┘  └─┘  └────
typ     └────┘  └─┘  └────
doc     └────┘  └─┘  └────
txt     └────┘  └─┘  └────
par     └────┘  └─┘  └────
pid                      
st   ─────────────────────
122  
src  
typ  
doc  
txt  
par  
pid  
st   
123  /-- If `f` is a multilinear map, then `f.to_linear_map m i` is the linear map obtained by fixing all
124  coordinates but `i` equal to those of `m`, and varying the `i`-th coordinate. -/
125  def to_linear_map (m : Πi, M₁ i) (i : ι) : M₁ i →ₗ[R] M₂ :=
id                             └┘            └┘  └─┘ └┘
src                                                  └─┘ 
typ                            └┘            └┘  └─┘ └┘
126  { to_fun := λx, f (update m i x),
id                    └────┘   
src                     └────┘
typ                   └────┘   
doc                     └────┘
127    add    := λx y, by simp,
id                 
src                       └──┘
typ                     └──┘
doc                       └──┘
txt                       └──┘
par                       └──┘
st                       └───┘
128    smul   := λc x, by simp }
id                 
src                       └───┘
typ                     └───┘
doc                       └───┘
txt                       └───┘
par                       └───┘
pid                           
st                       └────┘
129  
130  /-- In the specific case of multilinear maps on spaces indexed by `fin (n+1)`, where one can build
131  an element of `Π(i : fin (n+1)), M i` using `cons`, one can express directly the additivity of a
132  multilinear map along the first variable. -/
133  lemma cons_add (f : multilinear_map R M M₂) (m : Π(i : fin n), M i.succ) (x y : M 0) :
id                       └─────────────┘   └┘             └─┘     └───┘         
src                      └─────────────┘                    └─┘        └───┘
typ                      └─────────────┘   └┘             └─┘     └───┘         
doc                      └─────────────┘
134    f (cons (x+y) m) = f (cons x m) + f (cons y m) :=
id       └──┘         └──┘       └──┘  
src       └──┘             └──┘          └──┘
typ      └──┘         └──┘       └──┘  
doc       └──┘               └──┘           └──┘
135  by rw [← update_cons_zero x m (x+y), f.map_add, update_cons_zero, update_cons_zero]
id            └──────────────┘                   └──────────────┘  └──────────────┘
src     └────┘└──────────────┘     └─┘         └┘└──────────────┘└┘└──────────────┘└─
typ     └────┘└──────────────┘  └─┘└───────┘└┘└──────────────┘└┘└──────────────┘└─
doc     └────┘└──────────────┘      └─┘         └┘└──────────────┘└┘└──────────────┘└─
txt     └────┘                      └─┘         └┘                └┘                └─
par     └────┘                      └─┘         └┘                └┘                └─
pid       └──┘                      └─┘         └┘                └┘                
st     └───────────────────────────────┘└─────────┘└────────────────┘└────────────────┘
136  
src  
typ  
doc  
txt  
par  
pid  
st   
137  /-- In the specific case of multilinear maps on spaces indexed by `fin (n+1)`, where one can build
138  an element of `Π(i : fin (n+1)), M i` using `cons`, one can express directly the multiplicativity
139  of a multilinear map along the first variable. -/
140  lemma cons_smul (f : multilinear_map R M M₂) (m : Π(i : fin n), M i.succ) (c : R) (x : M 0) :
id                        └─────────────┘   └┘             └─┘     └───┘              
src                       └─────────────┘                    └─┘        └───┘
typ                       └─────────────┘   └┘             └─┘     └───┘              
doc                       └─────────────┘
141    f (cons (c • x) m) = c • f (cons x m) :=
id       └──┘             └──┘  
src       └──┘                  └──┘
typ      └──┘             └──┘  
doc       └──┘                     └──┘
142  by rw [← update_cons_zero x m (c • x), f.map_smul, update_cons_zero]
id            └──────────────┘                      └──────────────┘
src     └────┘└──────────────┘     └─┘          └┘└──────────────┘└─
typ     └────┘└──────────────┘  └─┘└────────┘└┘└──────────────┘└─
doc     └────┘└──────────────┘      └─┘          └┘└──────────────┘└─
txt     └────┘                      └─┘          └┘                └─
par     └────┘                      └─┘          └┘                └─
pid       └──┘                      └─┘          └┘                
st     └─────────────────────────────────┘└──────────┘└────────────────┘
143  
src  
typ  
doc  
txt  
par  
pid  
st   
144  end ring
145  
146  section comm_ring
147  
148  variables [comm_ring R] [∀i, add_comm_group (M₁ i)] [∀i, add_comm_group (M i)] [add_comm_group M₂]
id              └───────┘        └────────────┘            └────────────┘        └────────────┘
src             └───────┘         └────────────┘              └────────────┘         └────────────┘
typ             └───────┘        └────────────┘            └────────────┘        └────────────┘
149  [∀i, module R (M i)] [∀i, module R (M₁ i)] [module R M₂]
id       └────┘             └────┘           └────┘
src       └────┘               └────┘            └────┘
typ      └────┘             └────┘           └────┘
doc       └────┘               └────┘            └────┘
150  (f f' : multilinear_map R M₁ M₂)
id           └─────────────┘
src          └─────────────┘
typ          └─────────────┘
doc          └─────────────┘
151  
152  /-- If one multiplies by `c i` the coordinates in a finset `s`, then the image under a multilinear
153  map is multiplied by `s.prod c`. This is mainly an auxiliary statement to prove the result when
154  `s = univ`, given in `map_smul_univ`, although it can be useful in its own right as it does not
155  require the index set `ι` to be finite. -/
156  lemma map_piecewise_smul (c : ι → R) (m : Πi, M₁ i) (s : finset ι) :
id                                              └┘        └────┘ 
src                                                           └────┘
typ                                             └┘        └────┘ 
doc                                                           └────┘
157    f (s.piecewise (λi, c i • m i) m) = s.prod c • f m :=
id       └────────┘              └───┘    
src        └────────┘                     └───┘   
typ      └────────┘              └───┘    
doc        └────────┘                       └───┘
158  begin
st   └─────
159    refine s.induction_on (by simp) _,
id            └────────────┘
src    └─────┘└────────────┘   └──┘└─┘
typ    └─────┘└────────────┘   └──┘└─┘
doc    └─────┘└────────────┘   └──┘└─┘
txt    └─────┘                 └──┘└─┘
par    └─────┘                 └──┘└─┘
pid                           └──────┘
st   ──────────────────────────┘└───┘└─┘└─
160    assume j s j_not_mem_s Hrec,
src    └─────────────────────────┘
typ    └─────────────────────────┘
doc    └─────────────────────────┘
txt    └─────────────────────────┘
par    └─────────────────────────┘
pid    └─────────────────────────┘
st   ────────────────────────────┘└─
161    have A : function.update (s.piecewise (λi, c i • m i) m) j (m j) =
id              └─────────────┘                                       
src    └───────┘└─────────────┘              └─┘    └┘ └┘    └┘
typ    └───────┘└─────────────┘              └─┘    └┘ └┘   └┘
doc    └───────┘└─────────────┘              └─┘     └┘ └┘    └┘ 
txt    └───────┘                             └─┘     └┘ └┘    └┘ 
par    └───────┘                             └─┘     └┘ └┘    └┘ 
pid    └────┘└─┘                             └─┘     └┘ └┘    └┘ 
st   ─────────────────────────────────────────────────────────────────────
162             s.piecewise (λi, c i • m i) m,
id              └─────────┘                
src  ──────────┘└─────────┘  └─┘     └┘
typ  ──────────┘└─────────┘  └─┘    └┘
doc  ──────────┘└─────────┘  └─┘     └┘
txt  ──────────┘             └─┘     └┘
par  ──────────┘             └─┘     └┘
pid  ──────────┘             └─┘     └┘
st   ───────────────────────────────────────┘└─
163    { ext i,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ───┘└───┘└─
164      by_cases h : i = j,
id                       
src      └───────┘ └─┘  
typ      └───────┘ └─┘ 
doc      └───────┘ └─┘  
txt      └───────┘ └─┘  
par      └───────┘ └─┘  
pid               └─┘  
st   ─────────────────────┘└─
165      { rw h, simp [j_not_mem_s] },
id                    └─────────┘
src        └─┘   └────┘           └┘
typ        └─┘  └────┘└─────────┘└┘
doc        └─┘   └────┘           └┘
txt        └─┘   └────┘           └┘
par        └─┘   └────┘           └┘
pid                            
st   ─────┘└──┘└───────────────────┘└┘
166      { simp [h] } },
id               
src        └────┘ └┘
typ        └────┘└┘
doc        └────┘ └┘
txt        └────┘ └┘
par        └────┘ └┘
pid             
st   ──────────────┘└──┘
167    rw [s.piecewise_insert, f.map_smul, A, Hrec],
id                                           └──┘
src    └──┘                  └┘          └┘ └┘    
typ    └──┘└────────────────┘└┘└────────┘└┘└┘└──┘
doc    └──┘                  └┘          └┘ └┘    
txt    └──┘                  └┘          └┘ └┘    
par    └──┘                  └┘          └┘ └┘    
pid      └┘                  └┘          └┘ └┘    
st   ───────────────────────┘└──────────┘└─┘└────┘└──
168    simp [j_not_mem_s, mul_smul]
id           └─────────┘  └──────┘
src    └────┘           └┘└──────┘└┘
typ    └────┘└─────────┘└┘└──────┘└┘
doc    └────┘           └┘        └┘
txt    └────┘           └┘        └┘
par    └────┘           └┘        └┘
pid                   └┘        
st   ──────────────────────────────┘
169  end
st   └─┘
170  
171  /-- Multiplicativity of a multilinear map along all coordinates at the same time,
172  writing `f (λi, c i • m i)` as `univ.prod c • f m`. -/
173  lemma map_smul_univ [fintype ι] (c : ι → R) (m : Πi, M₁ i) :
id                        └─────┘                     └┘ 
src                       └─────┘
typ                       └─────┘                     └┘ 
doc                       └─────┘
174    f (λi, c i • m i) = finset.univ.prod c • f m :=
id                 └─────────┘└───┘    
src                      └─────────┘└───┘   
typ                └─────────┘└───┘    
doc                        └─────────┘└───┘
175  by simpa using map_piecewise_smul f c m finset.univ
id                  └────────────────┘    └─────────┘
src     └──────────┘└────────────────┘   └─────────┘
typ     └──────────┘└────────────────┘└─────────┘
doc     └──────────┘└────────────────┘   └─────────┘
txt     └──────────┘                                
par     └──────────┘                                
pid          └────┘                                
st     └─────────────────────────────────────────────────
176  
src  
typ  
doc  
txt  
par  
pid  
st   
177  /-- If one adds to a vector `m'` another vector `m`, but only for coordinates in a finset `t`, then
178  the image under a multilinear map `f` is the sum of `f (s.piecewise m m')` along all subsets `s` of
179  `t`. This is mainly an auxiliary statement to prove the result when `t = univ`, given in
180  `map_add_univ`, although it can be useful in its own right as it does not require the index set `ι`
181  to be finite.-/
182  lemma map_piecewise_add (m m' : Πi, M₁ i) (t : finset ι) :
id                                      └┘        └────┘ 
src                                                 └────┘
typ                                     └┘        └────┘ 
doc                                                 └────┘
183    f (t.piecewise (m + m') m') = t.powerset.sum (λs, f (s.piecewise m m')) :=
id       └────────┘    └┘  └┘   └───────┘└──┘       └────────┘  └┘
src        └────────┘               └───────┘└──┘          └────────┘
typ      └────────┘    └┘  └┘   └───────┘└──┘       └────────┘  └┘
doc        └────────┘                 └───────┘              └────────┘
184  begin
st   └─────
185    revert m',
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid          └─┘
st   ──────────┘└─
186    refine finset.induction_on t (by simp) _,
id            └─────────────────┘ 
src    └─────┘└─────────────────┘    └──┘└─┘
typ    └─────┘└─────────────────┘   └──┘└─┘
doc    └─────┘└─────────────────┘    └──┘└─┘
txt    └─────┘                       └──┘└─┘
par    └─────┘                       └──┘└─┘
pid                                 └──────┘
st   ─────────────────────────────────┘└───┘└─┘└─
187    assume i t hit Hrec m',
src    └────────────────────┘
typ    └────────────────────┘
doc    └────────────────────┘
txt    └────────────────────┘
par    └────────────────────┘
pid    └────────────────────┘
st   ───────────────────────┘└─
188    have A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i) :=
id               └────┘                            └────┘  └─────────┘                      └┘ 
src    └───────┘ └────┘  └──────────┘    └┘  └────┘ └─────────┘     └┘  └┘        └────
typ    └───────┘ └────┘  └──────────┘    └┘  └────┘ └─────────┘     └┘  └┘    └┘└────
doc    └───────┘         └──────────┘     └┘   └────┘ └─────────┘     └┘  └┘        └────
txt    └───────┘         └──────────┘     └┘                          └┘  └┘        └────
par    └───────┘         └──────────┘     └┘                          └┘  └┘        └────
pid    └────┘└─┘         └──────────┘     └┘                          └┘  └┘        └───
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
189      t.piecewise_insert _ _ _,
id       └────────────────┘
src  ───┘└────────────────┘└────┘
typ  ───┘└────────────────┘└────┘
doc  ───┘                  └────┘
txt  ───┘                  └────┘
par  ───┘                  └────┘
pid  ───┘                  └────┘
st   ───────────────────────────┘└─
190    have B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m',
id              └────┘                                     └─────────┘         └┘
src    └───────┘└────┘                 └┘  └┘     └┘ └─────────┘     └┘
typ    └───────┘└────┘                 └┘  └┘    └┘ └─────────┘    └┘└┘
doc    └───────┘└────┘                 └┘  └┘     └┘ └─────────┘     └┘
txt    └───────┘                       └┘  └┘     └┘                 └┘
par    └───────┘                       └┘  └┘     └┘                 └┘
pid    └────┘└─┘                       └┘  └┘     └┘                 └┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
191    { ext j,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ───┘└───┘└─
192      by_cases h : j = i,
id                       
src      └───────┘ └─┘  
typ      └───────┘ └─┘ 
doc      └───────┘ └─┘  
txt      └───────┘ └─┘  
par      └───────┘ └─┘  
pid               └─┘  
st   ─────────────────────┘└─
193      { rw h, simp [hit] },
id                    └─┘
src        └─┘   └────┘   └┘
typ        └─┘  └────┘└─┘└┘
doc        └─┘   └────┘   └┘
txt        └─┘   └────┘   └┘
par        └─┘   └────┘   └┘
pid                    
st   ─────┘└──┘└───────────┘└┘
194      { simp [h] } },
id               
src        └────┘ └┘
typ        └────┘└┘
doc        └────┘ └┘
txt        └────┘ └┘
par        └────┘ └┘
pid             
st   ──────────────┘└──┘
195    let m'' := update m' i (m i),
id                └────┘ └┘     
src    └─────────┘└────┘      
typ    └─────────┘└────┘└┘  
doc    └─────────┘└────┘      
txt    └─────────┘            
par    └─────────┘            
pid    └─────┘└─┘            
st   ─────────────────────────────┘└─
196    have C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m'',
id              └────┘                       └┘           └─────────┘          └─┘
src    └───────┘└────┘                 └┘  └┘    └┘ └─────────┘      └┘
typ    └───────┘└────┘                 └┘└┘└┘   └┘ └─────────┘     └┘└─┘
doc    └───────┘└────┘                 └┘  └┘    └┘ └─────────┘      └┘
txt    └───────┘                       └┘  └┘    └┘                  └┘
par    └───────┘                       └┘  └┘    └┘                  └┘
pid    └────┘└─┘                       └┘  └┘    └┘                  └┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
197    { ext j,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ───┘└───┘└─
198      by_cases h : j = i,
id                       
src      └───────┘ └─┘  
typ      └───────┘ └─┘ 
doc      └───────┘ └─┘  
txt      └───────┘ └─┘  
par      └───────┘ └─┘  
pid               └─┘  
st   ─────────────────────┘└─
199      { rw h, simp [m'', hit] },
id                    └─┘  └─┘
src        └─┘   └────┘   └┘   └┘
typ        └─┘  └────┘└─┘└┘└─┘└┘
doc        └─┘   └────┘   └┘   └┘
txt        └─┘   └────┘   └┘   └┘
par        └─┘   └────┘   └┘   └┘
pid                    └┘   
st   ─────┘└──┘└────────────────┘└┘
200      { by_cases h' : j ∈ t; simp [h, hit, m'', h'] } },
id                                   └─┘  └─┘  └┘
src        └───────┘  └─┘    └────┘ └┘   └┘   └┘  └┘
typ        └───────┘  └─┘  └────┘└┘└─┘└┘└─┘└┘└┘└┘
doc        └───────┘  └─┘     └────┘ └┘   └┘   └┘  └┘
txt        └───────┘  └─┘     └────┘ └┘   └┘   └┘  └┘
par        └───────┘  └─┘     └────┘ └┘   └┘   └┘  └┘
pid                  └─┘          └┘   └┘   └┘  
st   ─────────────────────────────────────────────────┘└──┘
201    rw [A, f.map_add, B, C, finset.sum_powerset_insert hit, Hrec, Hrec, add_comm],
id                          └────────────────────────┘ └─┘  └──┘  └──┘  └──────┘
src    └──┘ └┘         └┘ └┘ └┘└────────────────────────┘   └┘    └┘    └┘└──────┘
typ    └──┘└┘└───────┘└┘└┘└┘└────────────────────────┘└─┘└┘└──┘└┘└──┘└┘└──────┘
doc    └──┘ └┘         └┘ └┘ └┘                             └┘    └┘    └┘        
txt    └──┘ └┘         └┘ └┘ └┘                             └┘    └┘    └┘        
par    └──┘ └┘         └┘ └┘ └┘                             └┘    └┘    └┘        
pid      └┘ └┘         └┘ └┘ └┘                             └┘    └┘    └┘        
st   ──────┘└─────────┘└─┘└─┘└──────────────────────────────┘└────┘└────┘└────────┘└──
202    congr' 1,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          
st   ─────────┘└─
203    apply finset.sum_congr rfl (λs hs, _),
id           └──────────────┘ └─┘
src    └────┘└──────────────┘└─┘  └──────┘
typ    └────┘└──────────────┘└─┘  └──────┘
doc    └────┘                     └──────┘
txt    └────┘                     └──────┘
par    └────┘                     └──────┘
pid                              └──────┘
st   ──────────────────────────────────────┘└─
204    have : (insert i s).piecewise m m' = s.piecewise m m'',
id             └────┘                 └┘   └─────────┘  └─┘
src    └─────┘ └────┘  └──────────┘    └─────────┘ 
typ    └─────┘ └────┘ └──────────┘ └┘ └─────────┘└─┘
doc    └─────┘         └──────────┘    └─────────┘ 
txt    └─────┘         └──────────┘                
par    └─────┘         └──────────┘                
pid    └───┘└┘         └──────────┘                
st   ───────────────────────────────────────────────────────┘└─
205    { ext j,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ───┘└───┘└─
206      by_cases h : j = i,
id                       
src      └───────┘ └─┘  
typ      └───────┘ └─┘ 
doc      └───────┘ └─┘  
txt      └───────┘ └─┘  
par      └───────┘ └─┘  
pid               └─┘  
st   ─────────────────────┘└─
207      { rw h, simp [m'', finset.not_mem_of_mem_powerset_of_not_mem hs hit] },
id                    └─┘  └───────────────────────────────────────┘ └┘ └─┘
src        └─┘   └────┘   └┘└───────────────────────────────────────┘     └┘
typ        └─┘  └────┘└─┘└┘└───────────────────────────────────────┘└┘└─┘└┘
doc        └─┘   └────┘   └┘                                              └┘
txt        └─┘   └────┘   └┘                                              └┘
par        └─┘   └────┘   └┘                                              └┘
pid                    └┘                                              
st   ─────┘└──┘└─────────────────────────────────────────────────────────────┘└┘
208      { by_cases h' : j ∈ s; simp [h, m'', h'] } },
id                                    └─┘  └┘
src        └───────┘  └─┘     └────┘ └┘   └┘  └┘
typ        └───────┘  └─┘   └────┘└┘└─┘└┘└┘└┘
doc        └───────┘  └─┘     └────┘ └┘   └┘  └┘
txt        └───────┘  └─┘     └────┘ └┘   └┘  └┘
par        └───────┘  └─┘     └────┘ └┘   └┘  └┘
pid                  └─┘          └┘   └┘  
st   ────────────────────────────────────────────┘└──┘
209    rw this
id        └──┘
src    └─┘    
typ    └─┘└──┘
doc    └─┘    
txt    └─┘    
par    └─┘    
pid          
st   ─────────┘
210  end
st   └─┘
211  
212  /-- Additivity of a multilinear map along all coordinates at the same time,
213  writing `f (m + m')` as the sum  of `f (s.piecewise m m')` over all sets `s`. -/
214  lemma map_add_univ [fintype ι] (m m' : Πi, M₁ i) :
id                       └─────┘              └┘ 
src                      └─────┘
typ                      └─────┘              └┘ 
doc                      └─────┘
215    f (m + m') = (finset.univ : finset (finset ι)).sum (λs, f (s.piecewise m m')) :=
id         └┘    └─────────┘   └────┘  └────┘   └─┘        └────────┘  └┘
src                └─────────┘   └────┘  └────┘    └─┘           └────────┘
typ        └┘    └─────────┘   └────┘  └────┘   └─┘        └────────┘  └┘
doc                  └─────────┘   └────┘  └────┘                  └────────┘
216  by simpa using f.map_piecewise_add m m' finset.univ
id                  └─────────────────┘  └┘ └─────────┘
src     └──────────┘└─────────────────┘   └─────────┘
typ     └──────────┘└─────────────────┘└┘└─────────┘
doc     └──────────┘└─────────────────┘   └─────────┘
txt     └──────────┘                                 
par     └──────────┘                                 
pid          └────┘                                 
st     └─────────────────────────────────────────────────
217  
src  
typ  
doc  
txt  
par  
pid  
st   
218  instance : has_scalar R (multilinear_map R M₁ M₂) := ⟨λ c f,
id              └────────┘   └─────────────┘  └┘ └┘         
src             └────────┘    └─────────────┘
typ             └────────┘   └─────────────┘  └┘ └┘         
doc             └────────┘    └─────────────┘
219    ⟨λ m, c • f m, λm i x y, by simp [smul_add], λl i x d, by simp [smul_smul, mul_comm]⟩⟩
id                              └──────┘                  └───────┘  └──────┘
src                               └────┘└──────┘               └────┘└───────┘└┘└──────┘
typ                       └────┘└──────┘           └────┘└───────┘└┘└──────┘
doc                                └────┘                       └────┘         └┘        
txt                                └────┘                       └────┘         └┘        
par                                └────┘                       └────┘         └┘        
pid                                                                        └┘        
st                                └──────────────┘              └─────────────────────────┘
220  
221  @[simp] lemma smul_apply (c : R) (m : Πi, M₁ i) : (c • f) m = c • f m := rfl
id                                           └┘                   └─┘
src                                                                        └─┘
typ                                          └┘                   └─┘
doc    └──┘
222  
223  /-- The space of multilinear maps is a module over `R`, for the pointwise addition and scalar
224  multiplication. -/
225  instance : module R (multilinear_map R M₁ M₂) :=
id              └────┘   └─────────────┘  └┘ └┘
src             └────┘    └─────────────┘
typ             └────┘   └─────────────┘  └┘ └┘
doc             └────┘    └─────────────┘
226  module.of_core $ by refine { smul := (•), ..};
id   └────────────┘                       
src  └────────────┘      └─────┘ └───────┘└─────┘
typ  └────────────┘      └─────┘ └───────┘└─────┘
doc                      └─────┘ └───────┘ └─────┘
txt                      └─────┘ └───────┘ └─────┘
par                      └─────┘ └───────┘ └─────┘
pid                             └───────┘ └─────┘
st                      └───────────────────────────
227    intros; ext; simp [smul_add, add_smul, smul_smul]
id                        └──────┘  └──────┘  └───────┘
src    └────┘  └─┘  └────┘└──────┘└┘└──────┘└┘└───────┘└─
typ    └────┘  └─┘  └────┘└──────┘└┘└──────┘└┘└───────┘└─
doc    └────┘  └─┘  └────┘        └┘        └┘         └─
txt    └────┘  └─┘  └────┘        └┘        └┘         └─
par    └────┘  └─┘  └────┘        └┘        └┘         └─
pid                             └┘        └┘         
st   ────────────────────────────────────────────────────
228  
src  
typ  
doc  
txt  
par  
pid  
st   
229  variables (R ι)
230  
231  /-- The canonical multilinear map on `R^ι` when `ι` is finite, associating to `m` the product of
232  all the `m i` (multiplied by a fixed reference element `z` in the target module) -/
233  protected def mk_pi_ring [fintype ι] (z : M₂) : multilinear_map R (λ(i : ι), R) M₂ :=
id                             └─────┘        └┘    └─────────────┘              └┘
src                            └─────┘               └─────────────┘
typ                            └─────┘        └┘    └─────────────┘              └┘
doc                            └─────┘               └─────────────┘
234  { to_fun := λm, finset.univ.prod m • z,
id                  └─────────┘└───┘   
src                  └─────────┘└───┘   
typ                 └─────────┘└───┘   
doc                  └─────────┘└───┘
235    add    := λ m i x y, by simp [finset.prod_update_of_mem, add_mul, add_smul],
id                               └───────────────────────┘  └─────┘  └──────┘
src                            └────┘└───────────────────────┘└┘└─────┘└┘└──────┘
typ                        └────┘└───────────────────────┘└┘└─────┘└┘└──────┘
doc                            └────┘                         └┘       └┘        
txt                            └────┘                         └┘       └┘        
par                            └────┘                         └┘       └┘        
pid                                                         └┘       └┘        
st                            └──────────────────────────────────────────────────┘
236    smul   := λ m i c x, by { rw [smul_eq_mul], simp [finset.prod_update_of_mem, smul_smul, mul_assoc] } }
id                               └─────────┘         └───────────────────────┘  └───────┘  └───────┘
src                              └──┘└─────────┘  └────┘└───────────────────────┘└┘└───────┘└┘└───────┘└┘
typ                          └──┘└─────────┘  └────┘└───────────────────────┘└┘└───────┘└┘└───────┘└┘
doc                              └──┘             └────┘                         └┘         └┘         └┘
txt                              └──┘             └────┘                         └┘         └┘         └┘
par                              └──┘             └────┘                         └┘         └┘         └┘
pid                                └┘                                          └┘         └┘         
st                            └────────────────┘└────────────────────────────────────────────────────────┘└┘
237  
238  variables {R ι}
239  
240  @[simp] lemma mk_pi_ring_apply [fintype ι] (z : M₂) (m : ι → R) :
id                                   └─────┘        └┘          
src                                  └─────┘
typ                                  └─────┘        └┘          
doc    └──┘                          └─────┘
241    (multilinear_map.mk_pi_ring R ι z : (ι → R) → M₂) m = finset.univ.prod m • z := rfl
id      └────────────────────────┘             └┘    └─────────┘└───┘       └─┘
src     └────────────────────────┘                          └─────────┘└───┘         └─┘
typ     └────────────────────────┘             └┘    └─────────┘└───┘       └─┘
doc     └────────────────────────┘                           └─────────┘└───┘
242  
243  lemma mk_pi_ring_apply_one_eq_self [fintype ι]  (f : multilinear_map R (λ(i : ι), R) M₂) :
id                                       └─────┘         └─────────────┘              └┘
src                                      └─────┘          └─────────────┘
typ                                      └─────┘         └─────────────┘              └┘
doc                                      └─────┘          └─────────────┘
244    multilinear_map.mk_pi_ring R ι (f (λi, 1)) = f :=
id     └────────────────────────┘              
src    └────────────────────────┘                 
typ    └────────────────────────┘              
doc    └────────────────────────┘
245  begin
st   └─────
246    ext m,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
247    have : m = (λi, m i • 1), by { ext j, simp },
id                       
src    └─────┘   └─┘  └─┘       └───┘  └───┘
typ    └─────┘   └─┘ └─┘       └───┘  └───┘
doc    └─────┘    └─┘   └─┘       └───┘  └───┘
txt    └─────┘    └─┘   └─┘       └───┘  └───┘
par    └─────┘    └─┘   └─┘       └───┘  └───┘
pid    └───┘└┘    └─┘   └─┘          └┘      
st   ─────────────────────────┘     └────┘└─────┘└┘
248    conv_rhs { rw [this, f.map_smul_univ] },
id                    └──┘
src    └─────────┘└──┘    └┘               └┘
typ    └─────────┘└──┘└──┘└┘└─────────────┘└┘
txt    └─────────┘└──┘    └┘               └┘
par    └─────────┘└──┘    └┘               └┘
pid            └────┘    └┘               └─┘
st   ───────────┘└───────┘└───────────────┘ └┘
249    refl
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
250  end
st   └─┘
251  
252  variables (R ι M₂)
253  /-- When `ι` is finite, multilinear maps on `R^ι` with values in `M₂` are in bijection with `M₂`,
254  as such a multilinear map is completely determined by its value on the constant vector made of ones.
255  We register this bijection as a linear equivalence in `multilinear_map.pi_ring_equiv`. -/
256  protected def pi_ring_equiv [fintype ι]  : M₂ ≃ₗ[R] (multilinear_map R (λ(i : ι), R) M₂) :=
id                                └─────┘      └┘ └─┘  └─────────────┘              └┘
src                               └─────┘          └─┘   └─────────────┘
typ                               └─────┘      └┘ └─┘  └─────────────┘              └┘
doc                               └─────┘          └─┘   └─────────────┘
257  { to_fun    := λ z, multilinear_map.mk_pi_ring R ι z,
id                      └────────────────────────┘   
src                      └────────────────────────┘
typ                     └────────────────────────┘   
doc                      └────────────────────────┘
258    inv_fun   := λ f, f (λi, 1),
id                         
typ                        
259    add       := λ z z', by { ext m, simp [smul_add] },
id                     └┘                    └──────┘
src                              └───┘  └────┘└──────┘└┘
typ                    └┘       └───┘  └────┘└──────┘└┘
doc                              └───┘  └────┘        └┘
txt                              └───┘  └────┘        └┘
par                              └───┘  └────┘        └┘
pid                                 └┘              
st                            └──────┘└────────────────┘└┘
260    smul      := λ c z, by { ext m, simp [smul_smul, mul_comm] },
id                                         └───────┘  └──────┘
src                             └───┘  └────┘└───────┘└┘└──────┘└┘
typ                           └───┘  └────┘└───────┘└┘└──────┘└┘
doc                             └───┘  └────┘         └┘        └┘
txt                             └───┘  └────┘         └┘        └┘
par                             └───┘  └────┘         └┘        └┘
pid                                └┘               └┘        
st                           └──────┘└───────────────────────────┘└┘
261    left_inv  := λ z, by simp,
id                    
src                         └──┘
typ                        └──┘
doc                         └──┘
txt                         └──┘
par                         └──┘
st                         └───┘
262    right_inv := λ f, f.mk_pi_ring_apply_one_eq_self }
id                      └───────────────────────────┘
src                       └───────────────────────────┘
typ                     └───────────────────────────┘
263  
264  end comm_ring
265  
266  end multilinear_map
267  
268  section currying
269  /-!
270  ### Currying
271  
272  We associate to a multilinear map in `n+1` variables (i.e., based on `fin n.succ`) two
273  curried functions, named `f.curry_left` (which is a linear map on `E 0` taking values
274  in multilinear maps in `n` variables) and `f.curry_right` (wich is a multilinear map in `n`
275  variables taking values in linear maps on `E 0`). In both constructions, the variable that is
276  singled out is `0`, to take advantage of the operations `cons` and `tail` on `fin n`.
277  The inverse operations are called `uncurry_left` and `uncurry_right`.
278  
279  We also register linear equiv versions of these correspondences, in
280  `multilinear_curry_left_equiv` and `multilinear_curry_right_equiv`.
281  -/
282  open multilinear_map
283  
284  variables {R M M₂}
285  [comm_ring R] [∀i, add_comm_group (M i)] [add_comm_group M₂]
id    └───────┘        └────────────┘        └────────────┘
src   └───────┘         └────────────┘         └────────────┘
typ   └───────┘        └────────────┘        └────────────┘
286  [∀i, module R (M i)] [module R M₂]
id       └────┘          └────┘
src       └────┘           └────┘
typ      └────┘          └────┘
doc       └────┘           └────┘
287  
288  /-- Given a linear map `f` from `M 0` to multilinear maps on `n` variables,
289  construct the corresponding multilinear map on `n+1` variables obtained by concatenating
290  the variables, given by `m ↦ f (m 0) (tail m)`-/
291  def linear_map.uncurry_left
292    (f : M 0 →ₗ[R] (multilinear_map R (λ(i : fin n), M i.succ) M₂)) :
id             └─┘  └─────────────┘         └─┘     └───┘  └┘
src             └─┘   └─────────────┘          └─┘        └───┘
typ            └─┘  └─────────────┘         └─┘     └───┘  └┘
doc                    └─────────────┘
293    multilinear_map R M M₂ :=
id     └─────────────┘   └┘
src    └─────────────┘
typ    └─────────────┘   └┘
doc    └─────────────┘
294  { to_fun := λm, f (m 0) (tail m),
id                         └──┘ 
src                           └──┘
typ                        └──┘ 
doc                           └──┘
295    add    := λm i x y, begin
id                   
typ                  
st                         └─────
296      by_cases h : i = 0,
id                     
src      └───────┘ └─┘ └┘
typ      └───────┘ └─┘└┘
doc      └───────┘ └─┘  └┘
txt      └───────┘ └─┘  └┘
par      └───────┘ └─┘  └┘
pid               └─┘  
st   ─────────────────────┘└─
297      { revert x y,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid              └──┘
st   ─────┘└────────┘└─
298        rw h,
id            
src        └─┘
typ        └─┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────────┘└─
299        assume x y,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid        └────────┘
st   ───────────────┘└─
300        rw [update_same, update_same, update_same, f.map_add, add_apply,
id             └─────────┘  └─────────┘  └─────────┘             └───────┘
src        └──┘└─────────┘└┘└─────────┘└┘└─────────┘└┘         └┘└───────┘└─
typ        └──┘└─────────┘└┘└─────────┘└┘└─────────┘└┘└───────┘└┘└───────┘└─
doc        └──┘           └┘           └┘           └┘         └┘         └─
txt        └──┘           └┘           └┘           └┘         └┘         └─
par        └──┘           └┘           └┘           └┘         └┘         └─
pid          └┘           └┘           └┘           └┘         └┘         └─
st   ────────────────────┘└───────────┘└───────────┘└─────────┘└─────────┘└─
301            tail_update_zero, tail_update_zero, tail_update_zero] },
id             └──────────────┘  └──────────────┘  └──────────────┘
src  ─────────┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘
typ  ─────────┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘
doc  ─────────┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘
txt  ─────────┘                └┘                └┘                └┘
par  ─────────┘                └┘                └┘                └┘
pid  ─────────┘                └┘                └┘                
st   ─────────────────────────┘└────────────────┘└────────────────┘└┘
302      { rw [update_noteq (ne.symm h), update_noteq (ne.symm h), update_noteq (ne.symm h)],
id             └──────────┘  └─────┘    └──────────┘  └─────┘    └──────────┘  └─────┘ 
src        └──┘└──────────┘ └─────┘ └─┘└──────────┘ └─────┘ └─┘└──────────┘ └─────┘ └┘
typ        └──┘└──────────┘ └─────┘└─┘└──────────┘ └─────┘└─┘└──────────┘ └─────┘└┘
doc        └──┘                     └─┘                     └─┘                     └┘
txt        └──┘                     └─┘                     └─┘                     └┘
par        └──┘                     └─┘                     └─┘                     └┘
pid          └┘                     └─┘                     └─┘                     └┘
st   ─────────────────────────────────┘└────────────────────────┘└────────────────────────┘└──
303        revert x y,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid              └──┘
st   ───────────────┘└─
304        rw ← succ_pred i h,
id              └───────┘  
src        └───┘└───────┘ 
typ        └───┘└───────┘
doc        └───┘          
txt        └───┘          
par        └───┘          
pid          └─┘          
st   ───────────────────────┘└─
305        assume x y,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid        └────────┘
st   ───────────────┘└─
306        rw [tail_update_succ, map_add, tail_update_succ, tail_update_succ] }
id             └──────────────┘  └─────┘  └──────────────┘  └──────────────┘
src        └──┘└──────────────┘└┘└─────┘└┘└──────────────┘└┘└──────────────┘└┘
typ        └──┘└──────────────┘└┘└─────┘└┘└──────────────┘└┘└──────────────┘└┘
doc        └──┘└──────────────┘└┘       └┘└──────────────┘└┘└──────────────┘└┘
txt        └──┘                └┘       └┘                └┘                └┘
par        └──┘                └┘       └┘                └┘                └┘
pid          └┘                └┘       └┘                └┘                
st   ─────────────────────────┘└───────┘└────────────────┘└────────────────┘└─
307    end,
st   ────┘
308    smul := λm i c x, begin
id                 
typ                
st                       └─────
309      by_cases h : i = 0,
id                    
src      └───────┘ └─┘  └┘
typ      └───────┘ └─┘ └┘
doc      └───────┘ └─┘  └┘
txt      └───────┘ └─┘  └┘
par      └───────┘ └─┘  └┘
pid               └─┘  
st   ─────────────────────┘└─
310      { revert x,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid              └┘
st   ─────┘└──────┘└─
311        rw h,
id            
src        └─┘
typ        └─┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────────┘└─
312        assume x,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────────────┘└─
313        rw [update_same, update_same, tail_update_zero, tail_update_zero,
id             └─────────┘  └─────────┘  └──────────────┘  └──────────────┘
src        └──┘└─────────┘└┘└─────────┘└┘└──────────────┘└┘└──────────────┘└─
typ        └──┘└─────────┘└┘└─────────┘└┘└──────────────┘└┘└──────────────┘└─
doc        └──┘           └┘           └┘└──────────────┘└┘└──────────────┘└─
txt        └──┘           └┘           └┘                └┘                └─
par        └──┘           └┘           └┘                └┘                └─
pid          └┘           └┘           └┘                └┘                └─
st   ────────────────────┘└───────────┘└────────────────┘└────────────────┘└─
314            ← smul_apply, f.map_smul] },
id               └────────┘
src  ───────────┘└────────┘└┘          └┘
typ  ───────────┘└────────┘└┘└────────┘└┘
doc  ───────────┘          └┘          └┘
txt  ───────────┘          └┘          └┘
par  ───────────┘          └┘          └┘
pid  ───────────┘          └┘          
st   ─────────────────────┘└──────────┘└┘
315      { rw [update_noteq (ne.symm h), update_noteq (ne.symm h)],
id             └──────────┘  └─────┘    └──────────┘  └─────┘ 
src        └──┘└──────────┘ └─────┘ └─┘└──────────┘ └─────┘ └┘
typ        └──┘└──────────┘ └─────┘└─┘└──────────┘ └─────┘└┘
doc        └──┘                     └─┘                     └┘
txt        └──┘                     └─┘                     └┘
par        └──┘                     └─┘                     └┘
pid          └┘                     └─┘                     └┘
st   ─────────────────────────────────┘└────────────────────────┘└──
316        revert x,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid              └┘
st   ─────────────┘└─
317        rw ← succ_pred i h,
id              └───────┘  
src        └───┘└───────┘ 
typ        └───┘└───────┘
doc        └───┘          
txt        └───┘          
par        └───┘          
pid          └─┘          
st   ───────────────────────┘└─
318        assume x,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────────────┘└─
319        rw [tail_update_succ, tail_update_succ, map_smul] }
id             └──────────────┘  └──────────────┘  └──────┘
src        └──┘└──────────────┘└┘└──────────────┘└┘└──────┘└┘
typ        └──┘└──────────────┘└┘└──────────────┘└┘└──────┘└┘
doc        └──┘└──────────────┘└┘└──────────────┘└┘        └┘
txt        └──┘                └┘                └┘        └┘
par        └──┘                └┘                └┘        └┘
pid          └┘                └┘                └┘        
st   ─────────────────────────┘└────────────────┘└────────┘└─
320    end }
st   ────┘
321  
322  @[simp] lemma linear_map.uncurry_left_apply
doc    └──┘
323    (f : M 0 →ₗ[R] (multilinear_map R (λ(i : fin n), M i.succ) M₂)) (m : Πi, M i) :
id             └─┘  └─────────────┘         └─┘     └───┘  └┘            
src             └─┘   └─────────────┘          └─┘        └───┘
typ            └─┘  └─────────────┘         └─┘     └───┘  └┘            
doc                    └─────────────┘
324    f.uncurry_left m = f (m 0) (tail m) := rfl
id     └───────────┘          └──┘      └─┘
src     └───────────┘             └──┘       └─┘
typ    └───────────┘          └──┘      └─┘
doc     └───────────┘              └──┘
325  
326  /-- Given a multilinear map `f` in `n+1` variables, split the first variable to obtain
327  a linear map into multilinear maps in `n` variables, given by `x ↦ (m ↦ f (cons x m))`. -/
328  def multilinear_map.curry_left
329    (f : multilinear_map R M M₂) :
id          └─────────────┘   └┘
src         └─────────────┘
typ         └─────────────┘   └┘
doc         └─────────────┘
330    M 0 →ₗ[R] (multilinear_map R (λ(i : fin n), M i.succ) M₂) :=
id        └─┘  └─────────────┘         └─┘     └───┘  └┘
src        └─┘   └─────────────┘          └─┘        └───┘
typ       └─┘  └─────────────┘         └─┘     └───┘  └┘
doc               └─────────────┘
331  { to_fun := λx,
id                
typ               
332    { to_fun := λm, f (cons x m),
id                      └──┘  
src                       └──┘
typ                     └──┘  
doc                       └──┘
333      add    := λm i y y', by simp,
id                     └┘
src                              └──┘
typ                    └┘     └──┘
doc                              └──┘
txt                              └──┘
par                              └──┘
st                              └───┘
334      smul   := λm i y c, by simp },
id                     
src                             └───┘
typ                         └───┘
doc                             └───┘
txt                             └───┘
par                             └───┘
pid                                 
st                             └────┘
335    add := λx y, by { ext m, exact cons_add f m x y },
id                                  └──────┘    
src                      └───┘  └────┘└──────┘    
typ                    └───┘  └────┘└──────┘
doc                      └───┘  └────┘└──────┘    
txt                      └───┘  └────┘            
par                      └───┘  └────┘            
pid                         └┘                   
st                    └──────┘└───────────────────────┘└┘
336    smul := λc x, by { ext m, exact cons_smul f m c x } }
id                                   └───────┘    
src                       └───┘  └────┘└───────┘    
typ                     └───┘  └────┘└───────┘
doc                       └───┘  └────┘└───────┘    
txt                       └───┘  └────┘             
par                       └───┘  └────┘             
pid                          └┘                    
st                     └──────┘└────────────────────────┘└┘
337  
338  @[simp] lemma multilinear_map.curry_left_apply
doc    └──┘
339    (f : multilinear_map R M M₂) (x : M 0) (m : Π(i : fin n), M i.succ) :
id          └─────────────┘   └┘                      └─┘     └───┘
src         └─────────────┘                              └─┘        └───┘
typ         └─────────────┘   └┘                      └─┘     └───┘
doc         └─────────────┘
340    f.curry_left x m = f (cons x m) := rfl
id     └─────────┘      └──┘       └─┘
src     └─────────┘         └──┘         └─┘
typ    └─────────┘      └──┘       └─┘
doc     └─────────┘          └──┘
341  
342  @[simp] lemma linear_map.curry_uncurry_left
doc    └──┘
343    (f : M 0 →ₗ[R] (multilinear_map R (λ(i : fin n), M i.succ) M₂)) :
id             └─┘  └─────────────┘         └─┘     └───┘  └┘
src             └─┘   └─────────────┘          └─┘        └───┘
typ            └─┘  └─────────────┘         └─┘     └───┘  └┘
doc                    └─────────────┘
344    f.uncurry_left.curry_left = f :=
id     └───────────┘└─────────┘  
src     └───────────┘└─────────┘ 
typ    └───────────┘└─────────┘  
doc     └───────────┘└─────────┘
345  begin
st   └─────
346    ext m x,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid       └──┘
st   ────────┘└─
347    simp only [tail_cons, linear_map.uncurry_left_apply, multilinear_map.curry_left_apply],
id                └───────┘  └───────────────────────────┘  └──────────────────────────────┘
src    └─────────┘└───────┘└┘└───────────────────────────┘└┘└──────────────────────────────┘
typ    └─────────┘└───────┘└┘└───────────────────────────┘└┘└──────────────────────────────┘
doc    └─────────┘         └┘                             └┘                                
txt    └─────────┘         └┘                             └┘                                
par    └─────────┘         └┘                             └┘                                
pid        └──┘└┘         └┘                             └┘                                
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
348    rw cons_zero
id        └───────┘
src    └─┘└───────┘
typ    └─┘└───────┘
doc    └─┘         
txt    └─┘         
par    └─┘         
pid               
st   ──────────────┘
349  end
st   └─┘
350  
351  @[simp] lemma multilinear_map.uncurry_curry_left
doc    └──┘
352    (f : multilinear_map R M M₂) :
id          └─────────────┘   └┘
src         └─────────────┘
typ         └─────────────┘   └┘
doc         └─────────────┘
353    f.curry_left.uncurry_left = f :=
id     └─────────┘└───────────┘  
src     └─────────┘└───────────┘ 
typ    └─────────┘└───────────┘  
doc     └─────────┘└───────────┘
354  by { ext m, simp }
src       └───┘  └───┘
typ       └───┘  └───┘
doc       └───┘  └───┘
txt       └───┘  └───┘
par       └───┘  └───┘
pid          └┘      
st     └──────┘└─────┘└┘
355  
356  variables (R M M₂)
357  
358  /-- The space of multilinear maps on `Π(i : fin (n+1)), M i` is canonically isomorphic to
359  the space of linear maps from `M 0` to the space of multilinear maps on
360  `Π(i : fin n), M i.succ `, by separating the first variable. We register this isomorphism as a
361  linear isomorphism in `multilinear_curry_left_equiv R M M₂`.
362  
363  The direct and inverse maps are given by `f.uncurry_left` and `f.curry_left`. Use these
364  unless you need the full framework of linear equivs. -/
365  def multilinear_curry_left_equiv :
366    (M 0 →ₗ[R] (multilinear_map R (λ(i : fin n), M i.succ) M₂)) ≃ₗ[R] (multilinear_map R M M₂) :=
id         └─┘  └─────────────┘         └─┘     └───┘  └┘   └─┘  └─────────────┘   └┘
src         └─┘   └─────────────┘          └─┘        └───┘       └─┘   └─────────────┘
typ        └─┘  └─────────────┘         └─┘     └───┘  └┘   └─┘  └─────────────┘   └┘
doc                └─────────────┘                                 └─┘   └─────────────┘
367  { to_fun    := linear_map.uncurry_left,
id                  └─────────────────────┘
src                 └─────────────────────┘
typ                 └─────────────────────┘
doc                 └─────────────────────┘
368    add       := λf₁ f₂, by { ext m, refl },
id                   └┘ └┘
src                              └───┘  └───┘
typ                  └┘ └┘       └───┘  └───┘
doc                              └───┘  └───┘
txt                              └───┘  └───┘
par                              └───┘  └───┘
pid                                 └┘      
st                            └──────┘└─────┘└┘
369    smul      := λc f, by { ext m, refl },
id                    
src                            └───┘  └───┘
typ                          └───┘  └───┘
doc                            └───┘  └───┘
txt                            └───┘  └───┘
par                            └───┘  └───┘
pid                               └┘      
st                          └──────┘└─────┘└┘
370    inv_fun   := multilinear_map.curry_left,
id                  └────────────────────────┘
src                 └────────────────────────┘
typ                 └────────────────────────┘
doc                 └────────────────────────┘
371    left_inv  := linear_map.curry_uncurry_left,
id                  └───────────────────────────┘
src                 └───────────────────────────┘
typ                 └───────────────────────────┘
372    right_inv := multilinear_map.uncurry_curry_left }
id                  └────────────────────────────────┘
src                 └────────────────────────────────┘
typ                 └────────────────────────────────┘
373  
374  variables {R M M₂}
375  
376  /-- Given a multilinear map `f` in `n` variables to the space of linear maps from `M 0` to `M₂`,
377  construct the corresponding multilinear map on `n+1` variables obtained by concatenating
378  the variables, given by `m ↦ f (tail m) (m 0)`-/
379  def multilinear_map.uncurry_right (f : (multilinear_map R (λ(i : fin n), M i.succ) ((M 0) →ₗ[R] M₂))) :
id                                           └─────────────┘         └─┘     └───┘        └─┘ └┘
src                                          └─────────────┘          └─┘        └───┘         └─┘ 
typ                                          └─────────────┘         └─┘     └───┘        └─┘ └┘
doc                                          └─────────────┘
380    multilinear_map R M M₂ :=
id     └─────────────┘   └┘
src    └─────────────┘
typ    └─────────────┘   └┘
doc    └─────────────┘
381  { to_fun := λm, f (tail m) (m 0),
id                    └──┘    
src                     └──┘
typ                   └──┘    
doc                     └──┘
382    add    := λm i x y, begin
id                   
typ                  
st                         └─────
383      by_cases h : i = 0,
id                     
src      └───────┘ └─┘ └┘
typ      └───────┘ └─┘└┘
doc      └───────┘ └─┘  └┘
txt      └───────┘ └─┘  └┘
par      └───────┘ └─┘  └┘
pid               └─┘  
st   ─────────────────────┘└─
384      { revert x y,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid              └──┘
st   ─────┘└────────┘└─
385        rw h,
id            
src        └─┘
typ        └─┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────────┘└─
386        assume x y,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid        └────────┘
st   ───────────────┘└─
387        rw [tail_update_zero, tail_update_zero, tail_update_zero, update_same,
id             └──────────────┘  └──────────────┘  └──────────────┘  └─────────┘
src        └──┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘└─────────┘└─
typ        └──┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘└─────────┘└─
doc        └──┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘           └─
txt        └──┘                └┘                └┘                └┘           └─
par        └──┘                └┘                └┘                └┘           └─
pid          └┘                └┘                └┘                └┘           └─
st   ─────────────────────────┘└────────────────┘└────────────────┘└───────────┘└─
388            update_same, update_same, linear_map.map_add] },
id             └─────────┘  └─────────┘  └────────────────┘
src  ─────────┘└─────────┘└┘└─────────┘└┘└────────────────┘└┘
typ  ─────────┘└─────────┘└┘└─────────┘└┘└────────────────┘└┘
doc  ─────────┘           └┘           └┘                  └┘
txt  ─────────┘           └┘           └┘                  └┘
par  ─────────┘           └┘           └┘                  └┘
pid  ─────────┘           └┘           └┘                  
st   ────────────────────┘└───────────┘└──────────────────┘└┘
389      { rw [update_noteq (ne.symm h), update_noteq (ne.symm h), update_noteq (ne.symm h)],
id             └──────────┘  └─────┘    └──────────┘  └─────┘    └──────────┘  └─────┘ 
src        └──┘└──────────┘ └─────┘ └─┘└──────────┘ └─────┘ └─┘└──────────┘ └─────┘ └┘
typ        └──┘└──────────┘ └─────┘└─┘└──────────┘ └─────┘└─┘└──────────┘ └─────┘└┘
doc        └──┘                     └─┘                     └─┘                     └┘
txt        └──┘                     └─┘                     └─┘                     └┘
par        └──┘                     └─┘                     └─┘                     └┘
pid          └┘                     └─┘                     └─┘                     └┘
st   ─────────────────────────────────┘└────────────────────────┘└────────────────────────┘└──
390        revert x y,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid              └──┘
st   ───────────────┘└─
391        rw  [← succ_pred i h],
id                └───────┘  
src        └─────┘└───────┘  
typ        └─────┘└───────┘
doc        └─────┘           
txt        └─────┘           
par        └─────┘           
pid          └───┘           
st   ─────────────────────────┘└──
392        assume x y,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid        └────────┘
st   ───────────────┘└─
393        rw [tail_update_succ, map_add, tail_update_succ, tail_update_succ, linear_map.add_apply] }
id             └──────────────┘
src        └──┘└──────────────┘                                                                   └┘
typ        └──┘└──────────────┘                                                                   └┘
doc        └──┘└──────────────┘                                                                   └┘
txt        └──┘                                                                                   └┘
par        └──┘                                                                                   └┘
pid          └┘                                                                                   
st   ─────────────────────────┘                                                                   └─
394    end,
st   ────┘
395    smul := λm i c x, begin
id                 
typ                
st                       └───┘
396      by_cases h : i = 0,
397      { revert x,
398        rw h,
399        assume x,
400        rw [update_same, update_same, tail_update_zero, tail_update_zero, linear_map.map_smul] },
src                                                                                             
typ                                                                                             
doc                                                                                             
txt                                                                                             
par                                                                                             
pid                                                                                             
st                                                                                               
401      { rw [update_noteq (ne.symm h), update_noteq (ne.symm h)],
402        revert x,
403        rw [← succ_pred i h],
404        assume x,
405        rw [tail_update_succ, tail_update_succ, map_smul, linear_map.smul_apply] }
src                                                                               
typ                                                                               
doc                                                                               
txt                                                                               
par                                                                               
pid                                                                               
st                                                                                 └─
406    end }
st   ────┘
407  
408  @[simp] lemma multilinear_map.uncurry_right_apply
doc    └──┘
409    (f : (multilinear_map R (λ(i : fin n), M i.succ) ((M 0) →ₗ[R] M₂))) (m : Πi, M i) :
id           └─────────────┘         └─┘     └───┘        └─┘ └┘             
src          └─────────────┘          └─┘        └───┘         └─┘ 
typ          └─────────────┘         └─┘     └───┘        └─┘ └┘             
doc          └─────────────┘
410    f.uncurry_right m = f (tail m) (m 0) := rfl
id     └────────────┘     └──┘           └─┘
src     └────────────┘       └──┘             └─┘
typ    └────────────┘     └──┘           └─┘
doc     └────────────┘        └──┘
411  
412  /-- Given a multilinear map `f` in `n+1` variables, split the first variable to obtain
413  a multilinear map in `n` variables taking values in linear maps from `M 0` to `M₂`, given by
414  `m ↦ (x ↦ f (cons x m))`. -/
415  def multilinear_map.curry_right (f : multilinear_map R M M₂) :
id                                        └─────────────┘   └┘
src                                       └─────────────┘
typ                                       └─────────────┘   └┘
doc                                       └─────────────┘
416    multilinear_map R (λ(i : fin n), M i.succ) ((M 0) →ₗ[R] M₂) :=
id     └─────────────┘         └─┘     └───┘        └─┘ └┘
src    └─────────────┘          └─┘        └───┘         └─┘ 
typ    └─────────────┘         └─┘     └───┘        └─┘ └┘
doc    └─────────────┘
417  { to_fun := λm,
id                
typ               
418    { to_fun := λx, f (cons x m),
id                      └──┘  
src                       └──┘
typ                     └──┘  
doc                       └──┘
419      add    := λx y, by rw f.cons_add,
id                   
src                         └─┘
typ                       └─┘└┘
doc                         └─┘
txt                         └─┘
par                         └─┘
pid                           
st                         └────┘
420      smul   := λc x, by rw f.cons_smul },
id                   
typ                  
st                         
421    add := λm i x y, begin
id                 
typ                
422      ext z,
423      change f (cons z (update m i (x + y))) = f (cons z (update m i x)) + f (cons z (update m i y)),
id                                                                                                
typ                                                                                               
424      rw [cons_update, cons_update, cons_update, f.map_add]
st                                                           
425    end,
st     └─┘
426    smul := λm i c x, begin
id                  
typ                 
427      ext z,
428      change f (cons z (update m i (c • x))) = c • f (cons z (update m i x)),
id                                                                       
typ                                                                      
429      rw [cons_update, cons_update, f.map_smul]
st                                               
430    end }
st     └─┘
431  
432  @[simp] lemma multilinear_map.curry_right_apply
doc    └──┘
433    (f : multilinear_map R M M₂) (x : M 0) (m : Π(i : fin n), M i.succ) :
id                            └┘                       └┘      
src                                                       └┘
typ                           └┘                       └┘      
434    f.curry_right m x = f (cons x m) := rfl
435  
436  @[simp] lemma multilinear_map.curry_uncurry_right
doc    └──┘
437    (f : (multilinear_map R (λ(i : fin n), M i.succ) ((M 0) →ₗ[R] M₂))) :
id                                   └┘                          └┘
src                                   └┘
typ                                  └┘                          └┘
438    f.uncurry_right.curry_right = f :=
439  begin
440    ext m x,
441    simp only [cons_zero, multilinear_map.curry_right_apply, multilinear_map.uncurry_right_apply],
442    rw tail_cons
443  end
st   └─┘
444  
445  @[simp] lemma multilinear_map.uncurry_curry_right
doc    └──┘
446    (f : multilinear_map R M M₂) :
id                            └┘
typ                           └┘
447    f.curry_right.uncurry_right = f :=
448  by { ext m, simp }
st                    └┘
449  
450  variables (R M M₂)
451  
452  /-- The space of multilinear maps on `Π(i : fin (n+1)), M i` is canonically isomorphic to
453  the space of linear maps from the space of multilinear maps on `Π(i : fin n), M i.succ` to the space of linear
454  maps on `M 0`, by separating the first variable. We register this isomorphism as a
455  linear isomorphism in `multilinear_curry_right_equiv R M M₂`.
456  
457  The direct and inverse maps are given by `f.uncurry_right` and `f.curry_right`. Use these
458  unless you need the full framework of linear equivs. -/
459  def multilinear_curry_right_equiv :
460    (multilinear_map R (λ(i : fin n), M i.succ) ((M 0) →ₗ[R] M₂)) ≃ₗ[R] (multilinear_map R M M₂) :=
id                              └┘                          └┘                            └┘
src                              └┘
typ                             └┘                          └┘                            └┘
461  { to_fun    := multilinear_map.uncurry_right,
462    add       := λf₁ f₂, by { ext m, refl },
st                                           └┘
463    smul      := λc f, by { ext m, rw [smul_apply], refl },
id                   
typ                  
st                                                          └┘
464    inv_fun   := multilinear_map.curry_right,
465    left_inv  := multilinear_map.curry_uncurry_right,
466    right_inv := multilinear_map.uncurry_curry_right }
467  
468  end currying